A:Type, eq:EqDecider(A), B:(AType), f:fpf(A; a.B(a)), x:A, v:B(x).
((fpf-dom(eq; x; f)))  fpf-compatible(A; a.B(a); eq; fpf-single(x; v); f) 

latex

Definitions	fpf-compatible(A; a.B(a); eq; f; g), A, b, fpf-dom(eq; x; f), top, fpf(A; a.B(a)), EqDecider(T), fpf-single(x; v), x. t(x), x:A. B(x), P  Q, x(s), t  T
Lemmas	fpf-compatible-single, fpf-single wf, fpf-compatible-symmetry, deq wf, fpf wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, not wf